/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
/**
 * NuGat-API named Chameleon developed by Simon De Baets to Verimag.
 *
 */
package chameleon.model.NuGatStructure.fsm;

import chameleon.model.NuGatStructure.bdd.Bdd;
import chameleon.gameSolver.NuGat.NuGatInterface;
import chameleon.model.NuGatStructure.game.GamePlayer;
import chameleon.model.NuGatStructure.NuGatStructure;
import chameleon.model.NuGatStructure.enc.BddEnc;
import com.sun.jna.Pointer;

/**
 *
 * @author simon
 */
public class GameBddFsm extends NuGatStructure {

    public GameBddFsm(Pointer gameBddFsm, NuGatInterface nugat) {
        super(gameBddFsm,nugat);
    }
    
    public GameBddFsm(BddEnc enc,
                      BddFsm player_1,
                      Bdd stateVarCube_1,
                      Bdd stateFrozenVarCube_1,
                      BddFsm player_2,
                      Bdd stateVarCube_2,
                      Bdd stateFrozenVarCube_2,
                      NuGatInterface nugat){
        super(nugat.GameBddFsm_create(enc.ptr(),
                player_1.ptr(),
                stateVarCube_1.ptr(),
                stateFrozenVarCube_1.ptr(),
                player_2.ptr(),
                stateVarCube_2.ptr(),
                stateFrozenVarCube_2.ptr()),nugat);
    }

    @Override
    public GameBddFsm clone(){
        return new GameBddFsm(nugat_.GameBddFsm_copy(this.ptr()),nugat_);
    }
    
    /**
     * This function return a copy of the global gameBddFsm where the player 1
     * is different
     * @param fsm
     * @return 
     */
    
    public GameBddFsm changePLayer1(BddFsm fsm){
        return new GameBddFsm(fsm.getBddEncoding(), 
                fsm,
                getStateVarCube1(),
                getStateFrozenVarCube1(),
                getTransitionRelationPlayer2(),
                getStateVarCube2(),
                getStateFrozenVarCube2(),
                nugat_);
    }
    
    /**
     * This function return a copy of the global gameBddFsm where the player 2
     * is different
     * @param fsm
     * @return 
     */
    
    public GameBddFsm changePLayer2(BddFsm fsm){
        return new GameBddFsm(fsm.getBddEncoding(), 
                getTransitionRelationPlayer1(),
                getStateVarCube1(),
                getStateFrozenVarCube1(),
                fsm,
                getStateVarCube2(),
                getStateFrozenVarCube2(),
                nugat_);
    }
    
    /**
     * Return the transition relation to player 1
     *
     * @return bddFsm_ptr
     */

    public BddFsm getTransitionRelationPlayer1(){
        return new BddFsm (nugat_.GameBddFsm_get_player_1(this.ptr()),nugat_);
    }

    /**
     * Return the transition relation to player 2
     *
     * @return bddFsm_ptr
     */

    public BddFsm getTransitionRelationPlayer2(){
        return new BddFsm (nugat_.GameBddFsm_get_player_2(this.ptr()),nugat_);
    }

    public void printInfo(String fileName){
        nugat_.GameBddFsm_print_info(this.ptr(), nugat_.CmdOpenFile(fileName));
    }

    /**
     * Return the initial states to player 1
     *
     * @return BddStates
     */

    public Bdd getInit1(){
        return new Bdd (nugat_.GameBddFsm_get_init_1(this.ptr()),nugat_);
    }

    /**
     * Return the initial states to player 2
     *
     * @return BddStates
     */

    public Bdd getInit2(){
        return new Bdd (nugat_.GameBddFsm_get_init_2(this.ptr()),nugat_);
    }

    /**
     * Return the invariant states to player 1
     *
     * @return BddInvarStates
     */

    public Bdd getInvars1(){
        return new Bdd (nugat_.GameBddFsm_get_invars_1(this.ptr()),nugat_);
    }

    /**
     * Return the invariant states to player 2
     *
     * @return BddInvarStates
     */

    public Bdd getInvars2(){
        return new Bdd (nugat_.GameBddFsm_get_invars_2(this.ptr()),nugat_);
    }

    public Bdd getStateVarCube1(){
        return new Bdd(nugat_.GameBddFsm_get_state_var_cube_1(this.ptr()),nugat_);
    }
    
    public Bdd getStateVarCube2(){
        return new Bdd(nugat_.GameBddFsm_get_state_var_cube_2(this.ptr()),nugat_);
    }

    public Bdd getStateFrozenVarCube1(){
        return new Bdd(nugat_.GameBddFsm_get_state_frozen_var_cube_1(this.ptr()),nugat_);
    }
    
    public Bdd getStateFrozenVarCube2(){
        return new Bdd(nugat_.GameBddFsm_get_state_frozen_var_cube_2(this.ptr()),nugat_);
    }
    
    /**
     *
     * @param BddStates_goal
     * @param GamePlayer_player
     * @return BddStates
     */

    public Bdd getStrongBackwardImage (Bdd BddStates_goal,
                                               GamePlayer player){

        return  new Bdd (nugat_.GameBddFsm_get_strong_backward_image(this.ptr(),
                                                    BddStates_goal.ptr(),
                                                    player.ptr()),
                nugat_);

    }
    
    
    /**
     *  Synopsis    [ Returns a move of a player, which leads to a set of states. ]

  Description [ This method computes the set of current-next states
                which are legal (obey invars), there is (at least one)
                transition from current state to the next one, and the
                next state satisfy the given condition 'toState'.
                More accurately:

                For player 1 the returned formula is

                {<p1,p2,p1'> | Invar_1(p1) & Trans_1(p1,p2,p1')
                               & Invar_1(p1') & Invar_2(p1,p2)
                               & Exist p2',Trans_2(p1,p2,p1',p2')
                                           & Invar_2(p1',p2')
                               & Any p2',(Trans_2(p1,p2,p1',p2')
                                          & Invar_2(p1',p2'))
                                         -> toState(p1',p2') }

                This means that there must be at least one legal
                successor, and ALL possible moves of p2 go to
                'states'.

                For player 2:

                {<p1,p2,p1',p2'> | Invar_1(p1) & Trans_1(p1,p2,p1')
                                   & Invar_1(p1') & Invar_2(p1,p2)
                                   & Trans_2(p1,p2,p1',p2') & Invar_2(p1',p2')
                                   & toState(p1',p2') }

                Note: frozen variables do not participate in
                quantifications.

                The returned BDD is referenced. ]
     * @param bdd
     * @param player
     * @return 
     */

    public Bdd getMove(Bdd bdd, GamePlayer player) {
        return new Bdd( nugat_.GameBddFsm_get_move(this.ptr(), bdd.ptr(), player.ptr()),
                nugat_);
    }
    
    /**
     * Synopsis    [ Returns the set of states without successors. ]

  Description [ This method returns the set of states with no
                successor. Paramater 'player' defines for which player
                the no-successor states are computed. A state "ns" has
                no successor if all the following conditions hold: 1)
                ns is a state satisfying Invars for players. 2) no
                transition from ns exists which is leads to a state
                satisfying Invars for players.

                Formally, if p1 are the vars of first player and p2
                are the vars of the second player then the
                no-successor states for the first and second player
                are, respectively:

                NS_1 = {<p1,p2> | Invar_1(p1) & Invar_2(p1,p2)
                                  & not Exist p1'.Trans_1(p1,p2,p1')
                                                  & Invar_1(p1')}

                NS_2 =  {<p1,p2,p1'> | Invar_1(p1) & Invar_2(p1,p2)
                                       & Trans_1(p1,p2,p1') & Invar_1(p1')
                                       & not Exist p2'.Trans_2(p1,p2,p1',p2')
                                                       & Invar_2(p1',p2')}'

                The returned BDD belongs to this function. ]
     * @param player
     * @return 
     */
    
    public Bdd gameBddFsmWithoutSuccessorStates(GamePlayer player ){
        return new Bdd(nugat_.GameBddFsm_without_successor_states(this.ptr(), player.ptr()),
                nugat_);
    }

    /**Function********************************************************************

      Synopsis    [ The function returns a set of states such that a given
                    player can satisfy (stay in, choose) goal-states
                    taking into account interpretation (quantification) of
                    player roles and players' constraints. ]

      Description [ This function is the same as
                    GameBddFsm_can_player_satisfy but instead of returning
                    true or false returns a set of states.

                    The function has meaning only if there are variables
                    not belonging to current-state and frozen variable of
                    the given FSM. The players' variables are quantified
                    out and the returned BDD can consist only of that
                    external or next-state variables.

                    See the description of GameBddFsm_can_player_satisfy
                    for the exact definition of the result.

                    Invoker is responsible to de-reference the returned
                    BDD. ]

      SideEffects [ ]

      SeeAlso     [ GameBddFsm_can_player_satisfy ]

    ******************************************************************************/
    
    public Bdd gameBddFsmPlayerSatisfiesFrom(Bdd constr_1,
                                                Bdd constr_2,
                                                Bdd goalStates,
                                                GamePlayer player,
                                                char quantifiers){
        return new Bdd (nugat_.GameBddFsm_player_satisfies_from(this.ptr(),
                constr_1.ptr(), constr_2.ptr(), goalStates.ptr(),player.ptr(), quantifiers),nugat_);
    }
    
    
    /**
     * This function is wrapper to function GameBddFsm_can_player_satisfy.
     * We can not directly call this function because this function return
     * a boolean. But boolean return by this function are represent by a C enum.
     * So the return value of this function is not 0 or 1 but a pointer to this
     * enum. So the C function isTargetReached(..) call GameBddFsm_can_player_satisfy
     * and return 0 or 1. In this function we convert this 0 or 1 to a boolean
     * value.
      Synopsis    [ The function returns true if a given player can satisfy
                (stay in, choose) goal-states taking into account
                interpretation (quantification) of player roles and
                players' constraints. ]

        Description [ The interpretation of players' roles is given by
                parameter "quantifiers" (stored typically in
                opt_game_game_initial_condition).

                The formal description of the result is the following.

                If "quantifiers" is "N" (normal)
                for player 1:
                  Exist p1, constr_1(p1)
                            & Any p2, constr_2(p1,p2) -> GoalStates(p1,p2)
                for player 2:
                  Any p1, constr_1(p1)
                          -> Exist p2, constr_2(p1,p2) & GoalStates(p1,p2)

                If "quantifiers" is "A" (universal)
                for both players
                  Any p1, constr_1(p1)
                          -> (Any p2, constr_2(p1,p2) -> GoalStates(p1,p2))

                If "quantifiers" is "E" (existential)
                for both players
                  Exist p1, constr_1(p1)
                            & Exist p2, constr_2(p1,p2) & GoalStates(p1,p2)

                Note: there is no transition here.

                Note: p1 and p2 are both state and frozen variables.

                Note: all provided constraints must be already
                      conjoined with invariants, i.e.

                      constr_1 <= GameBddFsm_get_invars_1(),
                      constr_2 <= GameBddFsm_get_invars_2(),
                      goalStates <= GameBddFsm_get_invars_1()
                                    & GameBddFsm_get_invars_2().

                Note: all provided bdd_ptr are expected to have
                      current-state and frozen vars only, and contain
                      only the given Game FSM vars. Thus, the result
                      is always a constant. If there are other
                      variables see function
                      gameBddFsmPlayerSatisfiesFrom. ]
    
     * 
     * @param BddStates_constr_1
     * @param BddStates_constr_2
     * @param BddStates_goalStates
     * @param GamePlayer_player
     * @param quantifiers
     * @return
     */

    public boolean canPlayerSatisfy (Bdd constr_1,
                                            Bdd constr_2,
                                            Bdd goalStates,
                                            GamePlayer player,
                                            char quantifiers){

        int isTargetReached = nugat_.isTargetReached(this.ptr(), constr_1.ptr(),
                constr_2.ptr(),
                goalStates.ptr(),
                player.ptr(),
                quantifiers);

        if (isTargetReached == 1)
            return true;
        else if (isTargetReached == 0)
            return false;
        else
            throw new RuntimeException("NuGatManager :: boolean error");

    }
}
